COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00008 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.turn off "["
.turn off "{"
.TURN ON "→"
.turn on "α"
CS206∂(27)SOLUTIONS TO FINAL→FALL 1976

1. %2noccurl[x , u] ← qif qn u qthen 0 qelse [qif x = qa u qthen 1 qelse 0]
 + noccurl[x , qd u]%1.

2. %2noccurs[x , y] ← qif x = y qthen 1 qelse qif qat y qthen 0
qelse noccurs[x , qa y] + noccurs[x, qd y]%1.

3. There are many solutions to the %2samefringe%1 problem which has
been proposed as an example requiring co-routines.  Here one of the
simplest:

%2samefringe[x, y] ← x %3eq %2y ∨ [¬%3at %2x ∧
¬%3at %2y ∧ same[gopher x, gopher y]]

%2same[x, y] ← %3a %2x %3eq a %3y ∧
%2samefringe[%3d %2 x, %3d %2y]

%2gopher u ← %3if at a %2u %3then%2 u
%3else%2 gopher %3aa %2u . [%3da %2u . %3d %2u]
%1

%2gopher%1 digs up the first atom in an S-expression, piling
up the %2cdr%1s (with its hind legs) so that the indexing
through the atoms can be continued.
.nofill

4. %2prinb[e, l] ← qif qat e qthen e . l
∂(15)qelse %1LP%2 .
∂(20)[qif qn qd e qthen prinb[qa e, %1RP%2 . l]
∂(25)qelse qif qat qd e qthen prinb[qa e, %1DOT%2 . [qd e . [%1RP%2 . l]]]
∂(25)qelse prinb[qa e, qd prinb[qd e, l]]]%1

.fill
5. Let %2P(u)%1 be the assertion %2drop[u * v] = drop u * drop v%1.  The
induction principle is

	%2P[qnil] ∧ ∀u.[P[qd u] ⊃ P[u]] ⊃ ∀u.P[u]%1,

and putting %2P = λu.[drop[u * v] = drop u * drop v]%1 gives
.nofill

∂(10)%2[drop[qnil * v] = drop qnil * drop v]
∂(15)∧ ∀u.[drop[qd u * v] = drop qd u * drop v ⊃ drop[u * v] = drop u * drop v]

∂(10)⊃ ∀u.[drop[u * v] = drop u * drop v]%1.
.fill
We have 
.nofill

%2drop[qnil * v] ∂(15)= drop v ∂(40)%1by %2∀w.qnil * w = w,

∂(15)= qnil * drop v ∂(40) %1by same fact,

∂(15)= drop qnil * drop v ∂(40)drop qnil = qnil %1comes from def. of %2drop%1,

and the last equation is %2P[qnil]%1.  The induction step is

.skip to column 1
%2drop[u * v]∂(12) = drop[qif qn u qthen v qelse qa u .[q u * v]]→%1by def. %2u * v

∂(12)= qif qn u qthen drop v qelse drop[qa u . [qd u * v]]→%1by distrib. of c.e.%2

∂(12)= qif qn u qthen drop v qelse <qa [qa u . [qd u * v]]> . drop qd [qa u .[qd u * v]]
%1by def. of %2drop%1 and %2∀x y.¬qn[x . y]%1,

∂(12)= qif qn u qthen drop v qelse <qa u> . drop [qd u * v]→by qa and qd rules,%2

∂(12)= qif qn u qthen drop v qelse <qa u> . [drop qd u * drop v]→%1by induction hypothesis%2,

∂(12)= qif qn u qthen qnil * drop v qelse [<qa u> . drop qd u] * drop v
%1by %2∀w.[qnil * w = w]%1 and def. of %2[<qa u> . drop qd u] * drop v,

∂(12)= [qif qn u qthen qnil qelse <qa u> . drop qd u] * drop v→%1distrib. of c.e%2

∂(12)= drop u * drop v%1→%1by def. of %2drop v%1,
.fill
which is the result to be proved.
.nofill

6. %2compact x ← qa compact1[x, qnil]

compact1[x, u] ←∂(16){find[x, u]}[λz. 
∂(20)qif ¬qn z qthen qa z . u
∂(20)qelse qif qat x qthen x . u
∂(20)qelse α{compact1[qa x, u]}[λx1. 
∂(25){compact1[qd x, qd x1]}[λx2. 
∂(30)qif qa x qeq qa x1 ∧ qd x qeq qa x2 qthen x . [x . qd x2]
∂(30)qelse α{qa x1 . qa x2}[λv. v . [v . qd x2]]]]]

find[x, u] ← qif qn u qthen qNIL qelse qif x = qa u qthen u qelse find[x, qd u]
.fill
%1
	The following solution by Roy Harrington seems better than mine,
but I haven't taken time to analyze it:
.nofill

%2compact x ← comp[x, qNIL]

%2comp[x, y] ← ∂(13)qif qat x qthen x
∂(13)qelse {mem[x,y]}[λs.∂(30)qif ¬qn s qthen s
∂(30)qelse {comp[qd x, y]}[λz. comp[qa x, z . y] . z]]

mem[x, y] ← ∂(12)qif x = y qthen y
∂(12)qelse qif qat y qthen qNIL
∂(12)qelse {mem[x, qa y]}[λz. qif qn z qthen mem[x, qd y] qelse z]]